1 Preliminary Settings

To link up to the PAT library, several references have to be added into the project first. "PAT.Common" is an essential package that must be added in. The .dll file "PAT.Common.dll" is located at the root folder of your PAT installation. Then depending on the modules to be used, the corresponding references also need to be added. For example, if the CSP module is to be used, then "PAT.Module.CSP" should be included into the reference list. The .dll files can be found at "Modules" folder under the root. Note that the "Modules" folder itself also needs to be copied to the execution directory. If user defined C# library is to be imported to the model, then the .dll files of the library should be put under "Lib" folder of the execution directory.

2 Sample Codes

Below are some sample codes of how to use provided methods in the PAT library to run model verifications.

1. Load the module base of a specific module and parse the model specification using the loaded module base.
   • using PAT.Common;
   • using PAT.Common.Ultility;
   • using OutOfMemoryException = PAT.Common.Classes.Expressions.ExpressionClass.OutOfMemoryException;
   • using PAT.Common.Classes.Assertion;
   • using PAT.Common.Classes.Expressions.ExpressionClass;
   • using PAT.Common.Classes.LTS;
   • using PAT.Common.Classes.Ultility;
   • //Load the module
   • modulebase = PAT.Common.Ultility.Ultility.LoadModule("CSP");
   • //Parse the model specification
   • SpecificationBase Spec = modulebase.ParseSpecification(ModelSpecification, "", "");
2. After parsing, all the assertions in the model specification will be stored in the "SpecificationBase". The assertions can be retrieved by looking up in the generic library "SpecificationBase.AssertionDatabase". For instance, the following code will get the first assertion base from the assertion database.
   • AssertionBase assertion = Spec.AssertionDatabase.Values.ElementAt(0);
3. For each assertion, a series of settings can be applied before the verification. The settings include all the options that can be found in the GUI version, such as, fairness type, verbose, parallel verification, shortest witness trace, etc. Then call the method "InternalStart()" of "AssertionBase" to start the verification.
   • //Apply verification settings
   • assertion.UIInitialize(null, FairnessType.NO_FAIRNESS, false, false, false, true, false, false);
   • //Start the verification
   • assertion.InternalStart();
4. After the verification is done, the results will be stored in "AssertionBase.VerificationOutput". The results include "VerificationResult" which indicates whether the assertion is valid or not, "CounterExampleTrace" which keeps the witness trace of the counter example found, "EstimateMemoryUse" ,"VerificationTime", etc.
   • If (assertion.VerificationOutput.VerificationResult.Equals(VerificationResultType.INVALID))
   • {
     • //The assertion is invalid
   • }
   • //Get the counterexample trace
   • string result = "";
   • foreach (ConfigurationBase step in assertion.VerificationOutput.CounterExampleTrace)
   • {
     • result += step.GetDisplayEvent());
   • }
5. The "OutofMemoryException" should be caught in your code.
   • //RuntimeExceptions
   • catch (RuntimeException ex)
   • {
     • System.Console.Out.WriteLine("Runtime exception occurred: " + ex.Message);
     • //Out of memory Exception
     • if (ex is OutOfMemoryException)
     • {
       • System.Console.Out.WriteLine("Model is too big, out of memory.");
     • }
     • else
     • {
       • System.Console.Out.WriteLine("Check your input model for the possiblity of errors.");
     • }
   • }
   • //General Exceptions
   • catch (Exception ex)
   • {
     • System.Console.Out.WriteLine("Error occurred: " + ex.Message);
   • }

This section was contributed by Mr. Li Yi (liyi0630@gmail.com)